T:Type. 
(x,y:T. decidable((x = y)))
 (es:event_system{i:l}, e:es-E(es), x:Id.
 es-dtype(es; loc(e); x; T)
  (e'e.es-when(es; x; e') = es-when(es; x; e)  T
   e'<e.@e'(xes-when(es; x; e))
    e''(e',e].es-when(es; x; e'') = es-when(es; x; e)  T)) 

latex

Definitions

x:A. B(x), P  Q, es-dtype(es; i; x; T), P  Q, P  Q, es-locl(es; e; e'), t  T, prop{i:l}, x. t(x), A c B, ee'.P(e), T, True, guard(T), e<e'.P(e), x:A. B(x), e(e1,e2].P(e), @e(xv), wellfounded{i:l}(A; x,y.R(x;y)), x(s), decidable(P), A, P  Q, False

Lemmas

es-locl-wellfnd, event system-level-subtype, assert wf, es-isconst wf, es-vartype wf, alle-le wf, member wf, Id wf, es-loc wf, es-E wf, es-locl wf, es-when wf, subtype rel self, existse-before wf, es-change-to wf, alle-between3 wf, not wf, es-first wf, es-dtype wf, es-causl wf, event system wf, decidable wf, decidable assert, es-le wf, es-le-iff, es-after wf, es-pred wf, es-loc-pred, es-pred-locl, es-after-pred2, es-locl transitivity2, es-le weakening, squash wf, true wf, es-locl-iff